J:. 1  n < J. (1/n * n) < 2 

latex

Definitions

P  Q, i  j < k, {i..j}, , P & Q, x. t(x), T, P  Q, P  Q, False, A, True, (i = j), qeq(r;s), b, 0, r+gp, e, ff, i <z j, Y, (op,id) lb  i < ub. E(i),  lb  i < ub. E(i), tt, r + s, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, if b then t else f fi , b, a <p b, a < b, <+*>, (r) i  k < j. E(k), r * s, a  j < b. E(j), r < s, , {T}, P  Q, SQType(T), t  T, x:A. B(x), x(s), A  B, Dec(P), , S  T

Lemmas

qless transitivity 1 qorder, qless-int, qmul-qdiv-cancel, qmul zero qrng, mon ident q, qmul preserves qless, qinverse q, qadd inv assoc q, qadd comm q, qadd ac 1 q, qadd preserves qless, qadd wf, iff transitivity, int seg properties, qmul-mul, qmul-zero, qsub wf, le wf, qsum wf, qle wf, qsum-reciprocal-squares, int-eq-in-rationals, not functionality wrt iff, sum unroll base q, rationals wf, true wf, squash wf, qless wf, int-rational, int seg wf, qmul wf, int inc rationals, qdiv wf, nat wf, decidable int equal